Nuprl Lemma : sp_refl_cl_le_rel
13,42
postcript
pdf
T
:Type,
r
:(
T
T
). ((
r
)\)
>{
T
}
r
latex
Up
gen
algebra
1
Definitions of Statement
E
>{
T
}
E'
,
E
,
E
\
Definitions
t
T
,
P
Q
,
P
&
Q
,
P
Q
,
E
,
E
\
,
E
>{
T
}
E'
,
,
x
:
A
.
B
(
x
)
,
False
,
A
Lemmas
not
wf
origin
T:Type, r:(T
T
). ((r
)\) 
>{T} r T:Type, r:(TT). ((r)\) >{T} r >{T} E'
T
Q
Q>{T} E'x:A. B(x)
A